T:Type, L:(T List). ((null(L)))  (L = (firstn(||L|| - 1;L) @ [last(L)])) 

latex

Definitions	x:A. B(x), P  Q, b, null(as), as @ bs, firstn(n;as), ||as||, tt, ff, Y, if b then t else f fi , True, t  T, P  Q, , P & Q, P  Q, T, Top, S  T, last(L), l[i], hd(l), nth_tl(n;as), i z j, b, i <z j, A, False, , Unit,
Lemmas	not wf, true wf, false wf, lt int wf, length wf1, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le int wf, le wf, bnot wf, eqff to assert, squash wf, bnot of lt int, assert of le int, not functionality wrt iff, null wf3, top wf, assert of null, length zero, append wf, firstn wf, select cons tl, length cons, non neg length, select wf, last wf